perm filename SET[EKL,SYS]5 blob sn#825729 filedate 1986-10-09 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	useful set theory
C00006 00003	(proof setfacts)
C00013 ENDMK
C⊗;
;useful set theory
(wipe-out)
(get-proofs allp prf ekl sys)

(proof sets)
;all urelements will be S-expressions
;all S-expressions will be urelements

(decl (xv yv zv) (type: |ground|) (sort: urelement))
(decl (av bv) (type: |ground→truthval|))

(axiom |∀x.urelement x|)
(label simpinfo)

(axiom |∀xv.sexp(xv)|)
(label simpinfo)

(decl epsilon (type: |ground⊗@av→truthval|) (infixname: ε) (bindingpower: 925))
(define epsilon |∀av xv.xvεav≡av(xv)|)
(label epsilondef)

(axiom |∀av bv.(∀xv.xvεav≡xvεbv)⊃av=bv|)
(label set_extensionality)

(decl intersection (type: |@av⊗@av→@av|)
      (infixname: ∩) (bindingpower: 950) (prefixname: intersection))
(define intersection |∀av bv.av∩bv=λxv.(av(xv)∧bv(xv))|)
(label interdef)

(decl union (type: |@av⊗@av→@av|)
      (infixname: ∪) (bindingpower: 950) (prefixname: union))
(define union |∀av bv.av∪bv=λxv.(av(xv)∨bv(xv))|)
(label uniondef)

(decl inclusion (type: |@av⊗@av→truthval|)
      (infixname: ⊂) (bindingpower: 920) (prefixname: inclusion))
(define inclusion |∀av bv.av⊂bv≡∀xv.av(xv)⊃bv(xv)|)
(label inclusiondef)

(defax emptyset |emptyset=λxv.false|)
(defax emptyp |∀av.emptyp(av)=∀xv.¬av(xv)|)

;the set of occurrences of an S-exp

(decl mkset (type: |ground→@av|))
(define mkset |∀x.mkset(x)=(λyv.yv=x)|)
(label mkset_def)

;the set of members of a list

(decl mklset (type: |ground→@av|))
(define mklset |∀u.mklset(u)=λx.member(x,u)|)
(label mklsetdef)

(proof setfacts)

(axiom |∀u y.member(y,u)⊃mkset(y)⊂mklset u|)
(label mkset_mklset)

(axiom |∀av bv.av⊂bv∧bv⊂av⊃av=bv|)
(label double_inclusion)
(save-proofs set)